$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $L$:($T$ List).
\\[0ex]no\_repeats($T$;$L$) $\Rightarrow$ Inj(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} ;\{0..$\parallel$$L$$\parallel^{-}$\};$\lambda$$x$.index($L$;$x$))